<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Undergrad math in mathlib</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  

<div class="row mt-3">
        <div class="col">
                <h1>Undergraduate mathematics in mathlib</h1>

                <p>
				This gives pointers to undergraduate maths topics that are
				currently covered in mathlib.
				There is also a page listing undergraduate maths topics
				that are 
				<a href="undergrad_todo.html">not yet in mathlib</a>.
				</p>


                <div id="overview-accordion" class="accordion">
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0">
                                        <h5 class="card-title markdown-heading" id="0">
                                                <a role="button" data-toggle="collapse" href="#collapse-0" aria-expanded="false" aria-controls="collapse-0">
                                                        Linear algebra
                                                </a>
                                                <a class="hover-link" href="#0">#</a>
                                        </h5>
                                        <div id="collapse-0" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0-0">
                                        <h5 class="card-title markdown-heading" id="0-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-0-0" aria-expanded="false" aria-controls="collapse-0-0">
                                                        Fundamentals
                                                </a>
                                                <a class="hover-link" href="#0-0">#</a>
                                        </h5>
                                        <div id="collapse-0-0" class="collapse" data-parent="#overview-accordion-0 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/module/basic.html#vector_space" >vector space</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/module/prod.html#prod.semimodule" >product of vector spaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/module/basic.html#subspace" >vector subspace</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#submodule.quotient" >quotient space</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#submodule.complete_lattice" >sum of subspaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#submodule.exists_is_compl" >complementary subspaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#linear_independent" >linear independence</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#submodule.span" >generating sets</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#is_basis" >bases</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#exists_is_basis" >existence of bases</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/module/basic.html#linear_map" >linear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.range" >range of a linear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.ker" >kernel of a linear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/algebra.html#module.endomorphism_algebra" >algebra of endomorphisms of a vector space</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group" >general linear group</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0-1">
                                        <h5 class="card-title markdown-heading" id="0-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-0-1" aria-expanded="false" aria-controls="collapse-0-1">
                                                        Duality
                                                </a>
                                                <a class="hover-link" href="#0-1">#</a>
                                        </h5>
                                        <div id="collapse-0-1" class="collapse" data-parent="#overview-accordion-0 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/dual.html#module.dual" >dual vector space</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/dual.html#is_basis.dual_basis" >dual basis</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0-2">
                                        <h5 class="card-title markdown-heading" id="0-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-0-2" aria-expanded="false" aria-controls="collapse-0-2">
                                                        Finite-dimensional vector spaces
                                                </a>
                                                <a class="hover-link" href="#0-2">#</a>
                                        </h5>
                                        <div id="collapse-0-2" class="collapse" data-parent="#overview-accordion-0 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0-2" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#finite_dimensional" >finite-dimensionality</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#module_equiv_finsupp" >isomorphism with $K^n$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/dimension.html#rank" >rank of a linear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/dual.html#vector_space.eval_equiv" >isomorphism with bidual</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0-3">
                                        <h5 class="card-title markdown-heading" id="0-3">
                                                <a role="button" data-toggle="collapse" href="#collapse-0-3" aria-expanded="false" aria-controls="collapse-0-3">
                                                        Multilinearity
                                                </a>
                                                <a class="hover-link" href="#0-3">#</a>
                                        </h5>
                                        <div id="collapse-0-3" class="collapse" data-parent="#overview-accordion-0 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0-3" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/multilinear.html#multilinear_map" >multilinear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0-4">
                                        <h5 class="card-title markdown-heading" id="0-4">
                                                <a role="button" data-toggle="collapse" href="#collapse-0-4" aria-expanded="false" aria-controls="collapse-0-4">
                                                        Matrices
                                                </a>
                                                <a class="hover-link" href="#0-4">#</a>
                                        </h5>
                                        <div id="collapse-0-4" class="collapse" data-parent="#overview-accordion-0 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0-4" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/matrix/basic.html#matrix" >commutative-ring-valued matrices</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/matrix/basic.html#matrix" >field-valued matrices</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix.html#linear_map.to_matrix" >matrix representation of a linear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/determinant.html#matrix.det" >determinant</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/nonsingular_inverse.html#matrix.nonsing_inv" >invertibility</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-0-5">
                                        <h5 class="card-title markdown-heading" id="0-5">
                                                <a role="button" data-toggle="collapse" href="#collapse-0-5" aria-expanded="false" aria-controls="collapse-0-5">
                                                        Endomorphism polynomials
                                                </a>
                                                <a class="hover-link" href="#0-5">#</a>
                                        </h5>
                                        <div id="collapse-0-5" class="collapse" data-parent="#overview-accordion-0 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-0-5" class="accordion">
                                                                
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/field_theory/minimal_polynomial.html#minimal_polynomial" >minimal polynomial</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/char_poly.html#char_poly" >characteristic polynomial</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/char_poly.html#char_poly_map_eval_self" >Cayley-Hamilton theorem</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-1">
                                        <h5 class="card-title markdown-heading" id="1">
                                                <a role="button" data-toggle="collapse" href="#collapse-1" aria-expanded="false" aria-controls="collapse-1">
                                                        Group Theory
                                                </a>
                                                <a class="hover-link" href="#1">#</a>
                                        </h5>
                                        <div id="collapse-1" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-1" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-1-0">
                                        <h5 class="card-title markdown-heading" id="1-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-1-0" aria-expanded="false" aria-controls="collapse-1-0">
                                                        Basic definitions
                                                </a>
                                                <a class="hover-link" href="#1-0">#</a>
                                        </h5>
                                        <div id="collapse-1-0" class="collapse" data-parent="#overview-accordion-1 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-1-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/group/defs.html#group" >group</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/group/hom.html#monoid_hom" >group morphism</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/group/prod.html#prod.group" >direct product of groups</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#subgroup" >subgroup</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#subgroup.closure" >subgroup generated by a subset</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/group_theory/order_of_element.html" >order of an element</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/deprecated/subgroup.html#normal_subgroup" >normal subgroup</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/quotient_group.html#quotient_group.group" >quotient group</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action" >group action</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.stabilizer" >stabilizer of a point</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit" >orbit</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit_equiv_quotient_stabilizer" >quotient space</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-1-1">
                                        <h5 class="card-title markdown-heading" id="1-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-1-1" aria-expanded="false" aria-controls="collapse-1-1">
                                                        Abelian group
                                                </a>
                                                <a class="hover-link" href="#1-1">#</a>
                                        </h5>
                                        <div id="collapse-1-1" class="collapse" data-parent="#overview-accordion-1 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-1-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/order_of_element.html#is_cyclic" >cyclic group</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-1-2">
                                        <h5 class="card-title markdown-heading" id="1-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-1-2" aria-expanded="false" aria-controls="collapse-1-2">
                                                        Permutation group
                                                </a>
                                                <a class="hover-link" href="#1-2">#</a>
                                        </h5>
                                        <div id="collapse-1-2" class="collapse" data-parent="#overview-accordion-1 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-1-2" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/equiv/basic.html#equiv.perm" >permutation group of a type</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/group_theory/perm/sign.html#equiv.perm.sign" >signature</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-1-3">
                                        <h5 class="card-title markdown-heading" id="1-3">
                                                <a role="button" data-toggle="collapse" href="#collapse-1-3" aria-expanded="false" aria-controls="collapse-1-3">
                                                        Classical automorphism groups
                                                </a>
                                                <a class="hover-link" href="#1-3">#</a>
                                        </h5>
                                        <div id="collapse-1-3" class="collapse" data-parent="#overview-accordion-1 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-1-3" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group" >general linear group</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html#matrix.special_linear_group" >special linear group</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2">
                                        <h5 class="card-title markdown-heading" id="2">
                                                <a role="button" data-toggle="collapse" href="#collapse-2" aria-expanded="false" aria-controls="collapse-2">
                                                        Ring Theory
                                                </a>
                                                <a class="hover-link" href="#2">#</a>
                                        </h5>
                                        <div id="collapse-2" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2-0">
                                        <h5 class="card-title markdown-heading" id="2-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-2-0" aria-expanded="false" aria-controls="collapse-2-0">
                                                        Fundamentals
                                                </a>
                                                <a class="hover-link" href="#2-0">#</a>
                                        </h5>
                                        <div id="collapse-2-0" class="collapse" data-parent="#overview-accordion-2 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#ring" >ring</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/subring.html#is_subring" >subrings</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#ring_hom" >ring morphisms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/int/basic.html#int.comm_ring" >ring structure $\Z$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/ring/pi.html#pi.ring" >product of rings</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2-1">
                                        <h5 class="card-title markdown-heading" id="2-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-2-1" aria-expanded="false" aria-controls="collapse-2-1">
                                                        Ideals and Quotients
                                                </a>
                                                <a class="hover-link" href="#2-1">#</a>
                                        </h5>
                                        <div id="collapse-2-1" class="collapse" data-parent="#overview-accordion-2 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/ideals.html#ideal" >ideal of a commutative ring</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/ideals.html#ideal.quotient" >quotient rings</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/ideals.html#ideal.is_prime" >prime ideals</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/ideals.html#ideal.is_maximal" >maximal ideals</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/ideal_operations.html#ideal.quotient_inf_ring_equiv_pi_quotient" >Chinese remainder theorem</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2-2">
                                        <h5 class="card-title markdown-heading" id="2-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-2-2" aria-expanded="false" aria-controls="collapse-2-2">
                                                        Algebra
                                                </a>
                                                <a class="hover-link" href="#2-2">#</a>
                                        </h5>
                                        <div id="collapse-2-2" class="collapse" data-parent="#overview-accordion-2 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2-2" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/algebra.html#algebra" >algebra over a commutative ring</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2-3">
                                        <h5 class="card-title markdown-heading" id="2-3">
                                                <a role="button" data-toggle="collapse" href="#collapse-2-3" aria-expanded="false" aria-controls="collapse-2-3">
                                                        Divisibility in integral domains
                                                </a>
                                                <a class="hover-link" href="#2-3">#</a>
                                        </h5>
                                        <div id="collapse-2-3" class="collapse" data-parent="#overview-accordion-2 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2-3" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/associated.html#irreducible" >irreducible elements</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/invertible.html#invertible" >invertible elements</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/coprime.html#is_coprime" >coprime elements</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/ring_theory/unique_factorization_domain.html" >unique factorisation domain (UFD)</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/gcd_domain.html#gcd_domain.gcd" >greatest common divisor</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/gcd_domain.html#gcd_domain.lcm" >least common multiple</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/principal_ideal_domain.html#submodule.is_principal" >principal ideal domain</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html#euclidean_domain" >Euclidean rings</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/int/gcd.html#nat.xgcd" >Euclid's' algorithm</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html#int.euclidean_domain" >$\Z$ is a euclidean ring</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/int/modeq.html#int.modeq" >congruence in $\Z$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/associated.html#associates.prime" >prime numbers</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/zmod/basic.html#zmod.unit_of_coprime" >$\Z/n\Z$ and its invertible elements</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/nat/totient.html#nat.totient" >Euler's totient function ($\varphi$)</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2-4">
                                        <h5 class="card-title markdown-heading" id="2-4">
                                                <a role="button" data-toggle="collapse" href="#collapse-2-4" aria-expanded="false" aria-controls="collapse-2-4">
                                                        Polynomial rings
                                                </a>
                                                <a class="hover-link" href="#2-4">#</a>
                                        </h5>
                                        <div id="collapse-2-4" class="collapse" data-parent="#overview-accordion-2 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2-4" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/field_division.html#polynomial.euclidean_domain" >$K[X]$ is a euclidean ring when $K$ is a field</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/associated.html#irreducible" >irreducible polynomial</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/eisenstein_criterion.html#polynomial.irreducible_of_eisenstein_criterion" >Eisenstein's criterion</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/mv_polynomial.html#mv_polynomial" >polynomial algebra in one or several indeterminates over a commutative ring</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/ring_division.html#polynomial.roots" >roots of a polynomial</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/div.html#polynomial.root_multiplicity" >multiplicity</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/derivative.html#polynomial.derivative" >polynomial derivative</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-2-5">
                                        <h5 class="card-title markdown-heading" id="2-5">
                                                <a role="button" data-toggle="collapse" href="#collapse-2-5" aria-expanded="false" aria-controls="collapse-2-5">
                                                        Field Theory
                                                </a>
                                                <a class="hover-link" href="#2-5">#</a>
                                        </h5>
                                        <div id="collapse-2-5" class="collapse" data-parent="#overview-accordion-2 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-2-5" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/field.html#field" >fields</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/char_p.html#ring_char" >characteristic of a ring</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/char_zero.html#char_zero" >characteristic zero</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/char_p.html#char_p" >characteristic p</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/field_theory/subfield.html" >Subfields</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/char_p.html#frobenius" >Frobenius morphisms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/rat/basic.html#rat.division_ring" >field $\Q$ of rational numbers</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real.division_ring" >field $\R$ of real numbers</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/complex/basic.html#complex.field" >field $\C$ of complex numbers</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/complex/polynomial.html#complex.exists_root" >$\C$ is algebraically closed</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/localization.html#fraction_map" >field of fractions of an integral domain</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/algebraic.html#is_algebraic" >algebraic elements</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/algebraic.html#algebra.is_algebraic" >algebraic extensions</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/ring_theory/adjoin_root.html#adjoin_root" >rupture fields</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/field_theory/finite.html" >finite fields</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-3">
                                        <h5 class="card-title markdown-heading" id="3">
                                                <a role="button" data-toggle="collapse" href="#collapse-3" aria-expanded="false" aria-controls="collapse-3">
                                                        Bilinear and Quadratic Forms Over a Vector Space
                                                </a>
                                                <a class="hover-link" href="#3">#</a>
                                        </h5>
                                        <div id="collapse-3" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-3" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-3-0">
                                        <h5 class="card-title markdown-heading" id="3-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-3-0" aria-expanded="false" aria-controls="collapse-3-0">
                                                        Bilinear forms
                                                </a>
                                                <a class="hover-link" href="#3-0">#</a>
                                        </h5>
                                        <div id="collapse-3-0" class="collapse" data-parent="#overview-accordion-3 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-3-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form" >bilinear forms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#alt_bilin_form.is_alt" >alternating bilinear forms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#sym_bilin_form.is_sym" >symmetric bilinear forms</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form.to_matrix" >matrix representation</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form.to_matrix_comp" >change of coordinates</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-3-1">
                                        <h5 class="card-title markdown-heading" id="3-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-3-1" aria-expanded="false" aria-controls="collapse-3-1">
                                                        Quadratic forms
                                                </a>
                                                <a class="hover-link" href="#3-1">#</a>
                                        </h5>
                                        <div id="collapse-3-1" class="collapse" data-parent="#overview-accordion-3 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-3-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#quadratic_form" >quadratic form</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#quadratic_form.polar" >polar form of a quadratic</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-3-2">
                                        <h5 class="card-title markdown-heading" id="3-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-3-2" aria-expanded="false" aria-controls="collapse-3-2">
                                                        Orthogonality
                                                </a>
                                                <a class="hover-link" href="#3-2">#</a>
                                        </h5>
                                        <div id="collapse-3-2" class="collapse" data-parent="#overview-accordion-3 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-3-2" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form.is_ortho" >orthogonal elements</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-3-3">
                                        <h5 class="card-title markdown-heading" id="3-3">
                                                <a role="button" data-toggle="collapse" href="#collapse-3-3" aria-expanded="false" aria-controls="collapse-3-3">
                                                        Euclidean and Hermitian spaces
                                                </a>
                                                <a class="hover-link" href="#3-3">#</a>
                                        </h5>
                                        <div id="collapse-3-3" class="collapse" data-parent="#overview-accordion-3 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-3-3" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#inner_product_space" >Euclidean vector spaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#inner_mul_inner_self_le" >Cauchy-Schwarz inequality</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#inner_product_space.of_core.to_has_norm" >norm</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-3-4">
                                        <h5 class="card-title markdown-heading" id="3-4">
                                                <a role="button" data-toggle="collapse" href="#collapse-3-4" aria-expanded="false" aria-controls="collapse-3-4">
                                                        Endomorphisms
                                                </a>
                                                <a class="hover-link" href="#3-4">#</a>
                                        </h5>
                                        <div id="collapse-3-4" class="collapse" data-parent="#overview-accordion-3 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-3-4" class="accordion">
                                                                
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form.is_self_adjoint" >self-adjoint endomorphism</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-4">
                                        <h5 class="card-title markdown-heading" id="4">
                                                <a role="button" data-toggle="collapse" href="#collapse-4" aria-expanded="false" aria-controls="collapse-4">
                                                        Affine and Euclidian Geometry
                                                </a>
                                                <a class="hover-link" href="#4">#</a>
                                        </h5>
                                        <div id="collapse-4" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-4" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-4-0">
                                        <h5 class="card-title markdown-heading" id="4-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-4-0" aria-expanded="false" aria-controls="collapse-4-0">
                                                        General definitions
                                                </a>
                                                <a class="hover-link" href="#4-0">#</a>
                                        </h5>
                                        <div id="collapse-4-0" class="collapse" data-parent="#overview-accordion-4 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-4-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/affine_space.html#affine_space" >affine space</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/affine_space.html#affine_map" >affine function</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/affine_space.html#affine_subspace" >affine subspace</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/affine_space.html#finset.affine_combination" >barycenter</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/affine_space.html#affine_space.span_points" >affine span</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-4-2">
                                        <h5 class="card-title markdown-heading" id="4-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-4-2" aria-expanded="false" aria-controls="collapse-4-2">
                                                        Euclidean affine spaces
                                                </a>
                                                <a class="hover-link" href="#4-2">#</a>
                                        </h5>
                                        <div id="collapse-4-2" class="collapse" data-parent="#overview-accordion-4 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-4-2" class="accordion">
                                                                
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/geometry/euclidean.html#inner_product_geometry.angle" >angles of vectors</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5">
                                        <h5 class="card-title markdown-heading" id="5">
                                                <a role="button" data-toggle="collapse" href="#collapse-5" aria-expanded="false" aria-controls="collapse-5">
                                                        Single Variable Real Analysis
                                                </a>
                                                <a class="hover-link" href="#5">#</a>
                                        </h5>
                                        <div id="collapse-5" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-0">
                                        <h5 class="card-title markdown-heading" id="5-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-0" aria-expanded="false" aria-controls="collapse-5-0">
                                                        Real Numbers
                                                </a>
                                                <a class="hover-link" href="#5-0">#</a>
                                        </h5>
                                        <div id="collapse-5-0" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real" >definition of $\R$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real.division_ring" >field structure</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real.linear_order" >order</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-1">
                                        <h5 class="card-title markdown-heading" id="5-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-1" aria-expanded="false" aria-controls="collapse-5-1">
                                                        Sequences of real numbers
                                                </a>
                                                <a class="hover-link" href="#5-1">#</a>
                                        </h5>
                                        <div id="collapse-5-1" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html#filter.tendsto" >convergence</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/basic.html#map_cluster_pt" >limit point</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/core/init/core.html#nat" >recurrent sequences</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/order/liminf_limsup.html" >limit infimum and supremum</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/cauchy.html#cauchy_seq" >Cauchy sequences</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-2">
                                        <h5 class="card-title markdown-heading" id="5-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-2" aria-expanded="false" aria-controls="collapse-5-2">
                                                        Topology of R
                                                </a>
                                                <a class="hover-link" href="#5-2">#</a>
                                        </h5>
                                        <div id="collapse-5-2" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-2" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#real.metric_space" >metric structure</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/instances/real.html#real.complete_space" >completeness of R</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/sequences.html#tendsto_subseq_of_bounded" >Bolzano-Weierstrass theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#metric.compact_iff_closed_bounded" >compact subsets of $\R$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#set_of_is_preconnected_eq_of_ordered" >connected subsets of $\R$</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-3">
                                        <h5 class="card-title markdown-heading" id="5-3">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-3" aria-expanded="false" aria-controls="collapse-5-3">
                                                        Numerical Series
                                                </a>
                                                <a class="hover-link" href="#5-3">#</a>
                                        </h5>
                                        <div id="collapse-5-3" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-3" class="accordion">
                                                                
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/specific_limits.html#has_sum_geometric_of_abs_lt_1" >Geometric series</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-4">
                                        <h5 class="card-title markdown-heading" id="5-4">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-4" aria-expanded="false" aria-controls="collapse-5-4">
                                                        Real-valued functions defined on a subset of $\R$
                                                </a>
                                                <a class="hover-link" href="#5-4">#</a>
                                        </h5>
                                        <div id="collapse-5-4" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-4" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/basic.html#continuous" >continuity</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html#filter.tendsto" >limits</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#intermediate_value_Icc" >intermediate value theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/instances/real.html#real.image_Icc" >image of a segment</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-5">
                                        <h5 class="card-title markdown-heading" id="5-5">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-5" aria-expanded="false" aria-controls="collapse-5-5">
                                                        Differentiability
                                                </a>
                                                <a class="hover-link" href="#5-5">#</a>
                                        </h5>
                                        <div id="collapse-5-5" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-5" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html#has_deriv_at" >derivative at a point</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html#has_deriv_at" >differentiable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html#deriv.comp" >derivative of a composite function</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html#has_strict_deriv_at.of_local_left_inverse" >derivative of a reciprocal function</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/local_extr.html#exists_deriv_eq_zero" >Rolle's theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/mean_value.html#exists_ratio_deriv_eq_ratio_slope" >mean value theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/iterated_deriv.html#iterated_deriv" >higher order derivatives of functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/times_cont_diff.html#times_cont_diff" >$C^k$ functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html#deriv_mul" >Leibniz formula</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-7">
                                        <h5 class="card-title markdown-heading" id="5-7">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-7" aria-expanded="false" aria-controls="collapse-5-7">
                                                        Usual functions (trigonometric, rational, $\exp$, $\log$, etc)
                                                </a>
                                                <a class="hover-link" href="#5-7">#</a>
                                        </h5>
                                        <div id="collapse-5-7" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-7" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/eval.html#polynomial.eval" >polynomial functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/exp_log.html#real.log" >logarithms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/complex/exponential.html#real.exp" >exponential</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/algebra/group_power.html#monoid.pow" >power functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/complex/exponential.html#real.sin" >circular trigonometric functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/data/complex/exponential.html#real.sinh" >hyperbolic trigonometric functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/trigonometric.html#real.arcsin" >reciprocal circular trigonometric functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-9">
                                        <h5 class="card-title markdown-heading" id="5-9">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-9" aria-expanded="false" aria-controls="collapse-5-9">
                                                        Sequences and series of functions
                                                </a>
                                                <a class="hover-link" href="#5-9">#</a>
                                        </h5>
                                        <div id="collapse-5-9" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-9" class="accordion">
                                                                
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence.html#tendsto_uniformly" >uniform convergence</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence.html#continuous_of_uniform_approx_of_continuous" >continuity of the limit</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-5-10">
                                        <h5 class="card-title markdown-heading" id="5-10">
                                                <a role="button" data-toggle="collapse" href="#collapse-5-10" aria-expanded="false" aria-controls="collapse-5-10">
                                                        Convexity
                                                </a>
                                                <a class="hover-link" href="#5-10">#</a>
                                        </h5>
                                        <div id="collapse-5-10" class="collapse" data-parent="#overview-accordion-5 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-5-10" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/convex/basic.html#convex_on" >convex functions of a real variable</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/mean_value.html#convex_on_of_deriv2_nonneg" >characterizations of convexity</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/analysis/mean_inequalities.html" >convexity inequalities</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-7">
                                        <h5 class="card-title markdown-heading" id="7">
                                                <a role="button" data-toggle="collapse" href="#collapse-7" aria-expanded="false" aria-controls="collapse-7">
                                                        Topology
                                                </a>
                                                <a class="hover-link" href="#7">#</a>
                                        </h5>
                                        <div id="collapse-7" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-7" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-7-0">
                                        <h5 class="card-title markdown-heading" id="7-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-7-0" aria-expanded="false" aria-controls="collapse-7-0">
                                                        Topology and Metric Spaces
                                                </a>
                                                <a class="hover-link" href="#7-0">#</a>
                                        </h5>
                                        <div id="collapse-7-0" class="collapse" data-parent="#overview-accordion-7 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-7-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#metric.is_open_iff" >topology of a metric space</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/order.html#topological_space.induced" >induced topology</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#metric_space_pi" >finite product of metric spaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#metric.tendsto_at_top" >limits of sequences</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/basic.html#cluster_pt" >cluster points</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/basic.html#continuous" >continuous functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/homeomorph.html#homeomorph" >homeomorphisms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/subset_properties.html#compact_iff_finite_subcover" >compactness in terms of open covers (Borel-Lebesgue)</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/sequences.html#metric.compact_iff_seq_compact" >sequential compactness is equivalent to compactness (Bolzano-Weierstrass)</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/subset_properties.html#connected_space" >connectedness</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/subset_properties.html#connected_component" >connected components</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/lipschitz.html#lipschitz_with" >Lipschitz functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#metric.uniform_continuous_iff" >uniformly continuous functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/compact_separated.html#compact_space.uniform_continuous_of_continuous" >Heine-Cantor theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html#metric.complete_of_cauchy_seq_tendsto" >complete metric spaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/contracting.html#contracting_with.exists_fixed_point" >contraction mapping theorem</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-7-1">
                                        <h5 class="card-title markdown-heading" id="7-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-7-1" aria-expanded="false" aria-controls="collapse-7-1">
                                                        Normed vector spaces on $\R$ and $\C$
                                                </a>
                                                <a class="hover-link" href="#7-1">#</a>
                                        </h5>
                                        <div id="collapse-7-1" class="collapse" data-parent="#overview-accordion-7 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-7-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/basic.html#normed_space.topological_vector_space" >topology on a normed vector space</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/banach.html#open_mapping" >Banach open mapping theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/finite_dimension.html#linear_equiv.to_continuous_linear_equiv" >equivalence of norms in finite dimension</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/pi_Lp.html#pi_Lp.normed_space" >norms $\lVert\cdot\rVert_p$ on $\R^n$ and $\C^n$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/basic.html#summable_of_summable_norm" >absolutely convergent series in Banach spaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/algebra/module.html#continuous_linear_map" >continuous linear maps</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/operator_norm.html#linear_map.mk_continuous" >norm of a continuous linear map</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/metric_space/emetric_space.html#emetric.tendsto_uniformly_on_iff" >uniform convergence norm (sup-norm)</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/bounded_continuous_function.html#bounded_continuous_function.normed_space" >normed space of bounded continuous normed-space-valued functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/bounded_continuous_function.html#bounded_continuous_function.complete_space" >its completeness</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/finite_dimension.html#finite_dimensional.proper" >Heine-Borel theorem (closed bounded subsets are compact in finite dimension)</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/topology/bounded_continuous_function.html#bounded_continuous_function.arzela_ascoli" >Arzela-Ascoli theorem</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-7-2">
                                        <h5 class="card-title markdown-heading" id="7-2">
                                                <a role="button" data-toggle="collapse" href="#collapse-7-2" aria-expanded="false" aria-controls="collapse-7-2">
                                                        Hilbert Spaces
                                                </a>
                                                <a class="hover-link" href="#7-2">#</a>
                                        </h5>
                                        <div id="collapse-7-2" class="collapse" data-parent="#overview-accordion-7 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-7-2" class="accordion">
                                                                
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/dual.html#normed_space.dual.inst" >dual space</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-8">
                                        <h5 class="card-title markdown-heading" id="8">
                                                <a role="button" data-toggle="collapse" href="#collapse-8" aria-expanded="false" aria-controls="collapse-8">
                                                        Multivariable calculus
                                                </a>
                                                <a class="hover-link" href="#8">#</a>
                                        </h5>
                                        <div id="collapse-8" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-8" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-8-0">
                                        <h5 class="card-title markdown-heading" id="8-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-8-0" aria-expanded="false" aria-controls="collapse-8-0">
                                                        Differential Calculus
                                                </a>
                                                <a class="hover-link" href="#8-0">#</a>
                                        </h5>
                                        <div id="collapse-8-0" class="collapse" data-parent="#overview-accordion-8 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-8-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/fderiv.html#differentiable_on" >differentiable functions on an open subset of $\R^n$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/fderiv.html#fderiv" >differentials (linear tangent functions)</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/fderiv.html#fderiv.comp" >chain rule</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/mean_value.html#exists_ratio_deriv_eq_ratio_slope" >mean value theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/fderiv.html#differentiable" >differentiable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/times_cont_diff.html#times_cont_diff" >$k$-times continuously differentiable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/local_extr.html#is_local_min.fderiv_eq_zero" >local extrema</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/convex/basic.html#convex_on" >convexity of functions on an open convex subset of $\R^n$</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/geometry/manifold/charted_space.html#structomorph" >diffeomorphisms</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/inverse.html#has_strict_deriv_at.to_local_inverse" >inverse function theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/implicit.html#implicit_function_data.implicit_function" >implicit function theorem</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-9">
                                        <h5 class="card-title markdown-heading" id="9">
                                                <a role="button" data-toggle="collapse" href="#collapse-9" aria-expanded="false" aria-controls="collapse-9">
                                                        Measures and integral Calculus
                                                </a>
                                                <a class="hover-link" href="#9">#</a>
                                        </h5>
                                        <div id="collapse-9" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-9" class="accordion">
                                                                
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-9-0">
                                        <h5 class="card-title markdown-heading" id="9-0">
                                                <a role="button" data-toggle="collapse" href="#collapse-9-0" aria-expanded="false" aria-controls="collapse-9-0">
                                                        Measure theory
                                                </a>
                                                <a class="hover-link" href="#9-0">#</a>
                                        </h5>
                                        <div id="collapse-9-0" class="collapse" data-parent="#overview-accordion-9 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-9-0" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html#measurable_space" >measurable spaces</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html#measurable_space" >sigma-algebras</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html#measurable_space.pi" >product of sigma-algebras</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/borel_space.html#borel_space" >Borel sigma-algebras</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measure_space.html#measure_theory.measure" >positive measure</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measure_space.html#measure_theory.measure.count" >counting measure</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/lebesgue_measure.html#measure_theory.measure_theory.measure_space" >Lebesgue measure</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html#measurable_space.pi" >product measure</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html#measurable" >measurable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="/mathlib_docs/measure_theory/simple_func_dense.html" >approximation by step functions</a>
                        </span>
                        
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-9-1">
                                        <h5 class="card-title markdown-heading" id="9-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-9-1" aria-expanded="false" aria-controls="collapse-9-1">
                                                        Integration
                                                </a>
                                                <a class="hover-link" href="#9-1">#</a>
                                        </h5>
                                        <div id="collapse-9-1" class="collapse" data-parent="#overview-accordion-9 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-9-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/integration.html#measure_theory.lintegral" >integral of positive measurable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/integration.html#measure_theory.lintegral_infi_ae" >monotone convergence theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/integration.html#measure_theory.lintegral_liminf_le" >Fatou's lemma</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/l1_space.html#measure_theory.integrable" >integrable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/bochner_integration.html#measure_theory.tendsto_integral_of_dominated_convergence" >dominated convergence theorem</a>, 
                        </span>
                        
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/l1_space.html#measure_theory.integrable" >finite dimensional vector-valued integrable functions</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-10">
                                        <h5 class="card-title markdown-heading" id="10">
                                                <a role="button" data-toggle="collapse" href="#collapse-10" aria-expanded="false" aria-controls="collapse-10">
                                                        Probability Theory
                                                </a>
                                                <a class="hover-link" href="#10">#</a>
                                        </h5>
                                        <div id="collapse-10" class="collapse" data-parent="#overview-accordion">
                                                <div class="card-body">
                                                        <div id="overview-accordion-10" class="accordion">
                                                                
                        
						
                        
                        
                        
                        <div class="card statement-done">
                                <div class="card-header" id="heading-10-1">
                                        <h5 class="card-title markdown-heading" id="10-1">
                                                <a role="button" data-toggle="collapse" href="#collapse-10-1" aria-expanded="false" aria-controls="collapse-10-1">
                                                        Random variables and their laws
                                                </a>
                                                <a class="hover-link" href="#10-1">#</a>
                                        </h5>
                                        <div id="collapse-10-1" class="collapse" data-parent="#overview-accordion-10 ">
                                                <div class="card-body">
                                                        <div id="overview-accordion-10-1" class="accordion">
                                                                
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/probability_mass_function.html#pmf" >discrete law</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        <span class="statement-done">
                                <a  href="https://leanprover-community.github.io/mathlib_docs/measure_theory/probability_mass_function.html#pmf.bernoulli" >Bernoulli law</a>, 
                        </span>
                        
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                                                        </div>
                                                </div>
                                        </div>
                                </div>
                        </div>
                        
                        
                        
						
                        
                        
                        
						
                        
                        
                </div>
        </div>
</div>

  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>